Storm

Benchmark
Model:embedded v.1 (CTMC)
Parameter(s)MAX_COUNT = 8, T = 12
Property:actuators (prob-reach)
Invocation (default)
~/storm/build/bin/storm --prism embedded.prism --prop embedded.props actuators --constants MAX_COUNT=8,T=12 --prismcompat --exact floats --general:precision 1e-20  --engine portfolio --ddlib sylvan --sylvan:maxmem 6114 --sylvan:threads 4
Execution
Walltime:0.13852381706237793s
Return code:0
Note(s):The tool result '13162956974179480101883/125000000000000000000000' is tagged as incorrect. The reference result is '2486339329126654286603009697501669410565922080647235572297420531003436740865701642894224651957236979415804844019970070797212838741320749871087696043790430488516768144231337033817746564261751745074561347394006816495027017797689319547300488225074500148562849173672852142305219348461967484204844049064729196699735928014471258755257981315981437194941990940151801223037104684834501918219518509576147895594521550143080313306069328271572867233516691965651482621705351476665971739605138196440899155147689763504549588268208121401875264463514032072760483012146809591389917819090345027584564812047944749664670576370371539376963526238191240909958985452275278006429583432435031807238331342878089585624527146895090748546393263058273883548791148930403418281798548198424839109773636808627978181634014955673865189747661646872651996258392552936446048778850218123619968642035042613279480618036150872134108049644406926052409061681799637826350380022669199996003596956454782552145333056157894145489486150540020412367389756815095367155100979032989577219964876141639524244527608740339422128257119204903748534580255367130745069830155822896692205418889181867570399342666796568670310583910515081237965368477709014032538181219194690388788147910806457016503932544044361342482618424045300689342156932654513810653232/23611139712102051230917389163705830960031855919193061353466918264830083378326191986369644719731733927229539492600419384037259194731474764121283541927110582338954972260482489069672524784993784262550354865456872177586787640220120819688039079785300002792915291730955593483931646644219725546280035297145057925920216590907280123192615618204899469159482885775117640880607396241557854775904114044868093404127365731780383766098536743365431606149805147123738769862714193052746662633506746823832901275751745965930188386773348462353851130634494111719846304545619011283033383773694078253680336971342463788449790335853827682934039541430969389834393278233712786556823508225268957600063594542555015850051657407051988438160129534133247921531327619001040045086238243881240503946765414870850573700427770606192511529412103367398696559809991483002140786128316014280845971470100880405232693440182197432483126227685144563355464988202359315240457890538240804613319209327258473954661426136227180487183808347011148390279684571713981594509718194717843432940624635810976882203361528885015337153218704100617865345448218447207127579308191723103792137390005496384380796220104269395092237919302086773300230575431863081466614429004067089423894856968938002028941688162575178715549796054402371237245066557533118053584375' (approx. 0.1053036557931282) which means a relative error of '2.9215364927807575e-12' which is larger than the goal precision '1e-14'.
Relative Error:2.9215364927807575e-12
Log
Storm 1.5.1

Date: Tue Mar 17 15:09:58 2020
Command line arguments: --prism embedded.prism --prop embedded.props actuators --constants 'MAX_COUNT=8,T=12' --prismcompat --exact floats '--general:precision' 1e-20 --engine portfolio --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4
Current working directory: /

 WARN (GeneralSettings.cpp:110): Setting the precision option with module prefix does not effect all solvers. Consider setting --precision instead of --general:precision.
 WARN (Program.cpp:178): The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to use Markovian commands instead.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
Time for model input parsing: 0.004s.

 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
Portfolio engine picked the following settings: 
	engine=sparse	 bisimulation=false	 exact=false
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
 WARN (Program.cpp:1264): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
Time for model construction: 0.091s.

-------------------------------------------------------------- 
Model type: 	CTMC (sparse)
States: 	8034
Transitions: 	33564
Reward Models:  none
State Labels: 	4 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
   * down -> 5370 item(s)
   * fail_actuators -> 550 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "actuators": P=? [!("down") U "fail_actuators"] ...
Result (for initial states): 0.105303655793435840815064
Time for model checking: 0.014s.